\section{Stratégia vymazávania}

Na základe vety o úplnosti vieme, že ak máme nejakú množinu klauzúl $S$,
tak viem z nej postupne vytvárať rezolventy a ak nie je splniteľná, 
po konečnom počte krokov dostávam prázdnu klauzulu $\eps$.
Za účelom dôkazu teda musíme zaradom prehľadávať všetky rezolventy, ktoré
môže vzniknúť zo všetkých možných dvojíc klauzúl.

\begin{priklad}
    \label{prikl:vymazavanie}
    Majme množinu klauzúl $S=\{P\lor Q,\ \neg P\lor Q,\ 
        P \lor \neg Q,\ \neg P \lor \neg Q\}$. 
    Metódou rezolvent ukážte, že $S$ nie je splniteľná.

    \paragraph{Riešenie:}
    Použijeme takzvanú metódu nasýtenia -- budeme postupne 
    v každom kroku generovať najväčšiu možnú množinu rezolvent.
    Definujme si postupnosť $\{S^i\}_{i=0}^\infty$ množín klauzúl nasledovne:
    $S^0 = S$ a
    \begin{equation*}
        S^{n+1} = \{ \mbox{rezolventa klauzúl } C_1, C_2\ | \
            C_1 \in S^0 \union S^1 \union \cdots \union S^{n} \land
            C_2 \in S^n\},\quad n=1, 2, \dots
    \end{equation*}
    Takýmto spôsobom by sme po $39$ krokoch dostali prázdnu klauzulu.
    Problém tejto metódy je, že niektoré klauzuly sa vyskytnú v
    popísanom prístupe viackrát. Prípadne sa tam môžu vyskytnúť tautológie.
\end{priklad}

Videli sme, že predchádzajúca metóda nie je úplne optimálna. Preto za
účelom rýchlejšieho prehľadávania budeme niektoré evidentne nadbytočné
rezolventy zahadzovať (a algoritmus nazveme stratégiou vymazávania).
Najskôr si zadefinujeme, ako si budeme predstavovať nadbytočné rezolventy.

\begin{definicia}[podklauzula]
    Klauzula $C$ je podklauzulou klauzuly $D$ (alebo tiež $C$ pohlcuje
    $D$) práve vtedy, keď existuje substitúcia $\sigma$ taká, že platí $C\sigma
    \subseteq D$. Klauzulu $D$ vtedy tiež nazývame nadklauzulou klauzuly $C$.
\end{definicia}

\begin{priklad}
    Majme klauzuly $C = P(x)$ a $D = P(a) \lor Q(a)$.
    Ak budeme uvažovať substitúciu $\sigma = \{a/x\}$, dostaneme
    $C\sigma = P(a)$ a teda $C\sigma \subseteq D$.
    Čiže $C$ je podklauzula $D$.
\end{priklad}

\begin{poznamka}
    Ak $D$ je identicky rovná $C$ alebo ak klauzula $D$ je inštancia $C$, 
    potom $D$ je nadklauzula $C$.
\end{poznamka}


Ako sme už teda povedali, stratégia vymazávania spočíva vo vylepšení metódy
nasýtenia o zahadzovanie zbytočných výsledkov.
Čiže opäť konštruujeme postupnosť $\{S^i\}_{i=0}$.
Do $S^{n+1}$ ale teraz vyberieme iba tie rezolventy $C_1, C_2$ 
(opäť $C_1 \in (S^0 \union S^1 \union \dots \union S^n)$ a $C_2 \in S^n$),
ktoré nie sú tautológie a ani nadklauzuly niektorej z klauzúl dosiahnutej
doteraz.

\begin{priklad}[Revízia \ref{prikl:vymazavanie}]
    Opäť máme množinu klauzúl $S=\{P\lor Q,\ \neg P\lor Q,\ 
        P \lor \neg Q,\ \neg P \lor \neg Q\}$.

    \begin{itemize}
    %%% {{{
    \item[$S^0:$]
        \begin{itemize}
            \item[1] $P\lor Q$
            \item[2] $\neg P \lor Q$
            \item[3] $P\lor \neg Q$
            \item[4] $\neg P \lor \neg Q$
        \end{itemize}

    \item[$S^1:$]
        \begin{itemize}
        \item[5] $Q$ -- rezolventa 1, 2
        \item[6] $P$ -- rezolventa 1, 3
        \item[7] $\neg P$ -- rezolventa 2, 4
        \item[8] $\neg Q$ -- rezolventa 3, 4
        \end{itemize}

    \item[$S^2:$]
        \begin{itemize}
            \item[$\vdots$] -- zahodíme veľa rezolvent, napr. rezolventa
                1,8 je $P \lor \eps \equiv P$ a tú už máme.
            \item[9] $\eps$ -- rezolventa 5,8
        \end{itemize}
    %%% }}}
    \end{itemize}
\end{priklad}

\subsection{Algoritmus  pohltenia}
Jediný problém, ktorý nám ostáva vyriešiť je detekcia či je nejaká
klauzula tautológia alebo či je podformulou inej klauzuly. Prvý prípad
sa rieši jednoducho -- tautológiu máme práve vtedy, ak sa vo formule
vyskytuje kontrárna dvojica. S podformulou to bude horšie.
Skúsme sa na to pozrieť takto:

Nech $C$, $D$ sú klauzuly. Označme si substitúciu premenných v D za
nové konštanty (nevyskytujúce sa v $C$, $D$) ako
\begin{equation*}
    \Theta = \{ a_1 / x_1,\ a_2 / x_2,\ \ldots,\ a_n / x_n \}
\end{equation*}
%
Ak je klauzula $D$ tvaru
\begin{equation*}
    D = L_1 \lor L_2 \lor \ldots \lor L_m
\end{equation*}
dostávame, že $D\Theta$ je základná klauzula (neobsahujúca premenné).
%
\begin{equation*}
    D \Theta = L_1\Theta \lor L_2 \Theta \lor \ldots \lor L_m \Theta
\end{equation*}
%
Nás bude zaujímať jej negácia
\begin{equation*}
\neg D\Theta = \neg L_1 \Theta \land \neg L_2 \Theta 
                \land \ldots \land \neg L_m \Theta
\end{equation*}
%
Algoritums, ktorý preveruje, či klauzula $C$ je podklauzulou $D$ bude
vyzerať nasledovne:

\begin{enumerate}
    \item Nech 
        $W = \{ \neg L_1 \Theta, \neg L_2 \Theta, \ldots, \neg L_m \Theta \}$
        a nech $k=0$ a $U^0 = \{ C \}$

    \item Ak $U^k$ obsahuje $\eps$, tak algoritmus skončí
        s výsledkom, že $C$ je pod $D$.

    \item V opačnom prípade kladieme 
        \begin{equation*}
            U^{k+1} = \{ \mbox{rezolventa } C_1 \mbox{ a } C_2 | 
            C_1 \in U^{k} \land C_2 \in W\}
        \end{equation*}

    \item Ak $U^{k+1}$ je $\emptyset$, tak algoritmus skončí s
        výsledkom, že  $C$ nie je podklauzula $D$. 

    \item V opačnom prípade kladieme $k=k+1$ a opakujeme krok 2
\end{enumerate}

\startFIXME

\begin{poznamka}
    $\mathcal{U}^k, \mathcal{U}^{k+1}$, klauzuly z
    $\mathcal{U}^{k}$ sú konečné. $\mathcal{U}^0, \mathcal{U}^1, \ldots \square$.
\end{poznamka}

\begin{dokaz}
    Predpokladajme, že $C$ je podklauzula $D$. Na základe našej
    definície existuje substitúcia $\sigma$, že $C\sigma \subseteq D$. Teda
    $C(\sigma \circ \Theta) \subseteq D\Theta$. Literály z $C\sigma \circ \Theta$
    môžeme vynechať pomocou jednotkových klauzúl z $W$. ... Algoritmus skončí svoju
    činnosť.
    \par
    Obrátené tvrdenie: predpokladajme, že algoritmus zakončuje prácu na treťom
    kroku. Odmietnutie môžeme znázorniť nasledujúcim obrázkom:

    \todo{obrazok}

    $$C_0, N_1 ,\ldots B_r \in W$$
    $$C(\sigma_0 \circ \sigma_1 \circ \sigma \circ \sigma_r) = \{ \neg B_0, \neg
    B_1, \ldots \neg B_r\} \subseteq D\Theta$$
    $$\lambda = \sigma_0 \circ \sigma_1 \circ \sigma_2 \ldots \circ \sigma_r \implies
    C \lambda \subseteq D\Theta$$

    $\sigma$, ktorá dostaneme z $\lambda$ tak, že v každom komponente $\lambda$
    nahradíme  konštantu $a_i$ premennou $x_i$, $i=1, 2, 3, \ldots$. $C\sigma
    \subseteq D$. $C$ je pod $D$.
\end{dokaz}

\begin{priklad}
    Majme
    \begin{align*}
      C &= \neg P(x) \,\lor\, Q(f(x),a) \\
      D &= \neg P(h(y)) \,\lor\, Q(f(h(y)),a) \,\lor\, P(z)
    \end{align*}
    Zistite, či klauzula $C$ je podklauzulou $D$.

    Začneme tým, že $y$ a $z$ sú premenné v $D$. Spravíme preto substitúciu
    $\Theta = \{ b/y, c/z\}$ kde konštanty $b$, $c$
    nevystupujú v $C$ ani $D$. Najprv vypočítame
    $D\Theta = \neg P(h(b)) \,\lor\, Q(f(h(b)),a) \,\lor\, \neg P(c)$
    Čiže
    $$\neg D \Theta = P(h(b)) \,\land\, \neg Q(f(h(b)),a) \,\land\, P(c)$$
    A teda máme množiny
    \begin{align*}
      W &= \{P(h(b)),\, \neg Q(f(h(b)),a),\, P(c) \} \\
      U^0 &= \{C\} = \{\neg P(x) \,\lor\, Q(f(x),a)\}
    \end{align*}
    $U^0$ neobsahuje $\eps$ a teda musíme vytvoriť $\mathcal{U}^1$. Urobíme
    príslušnú substitúciu v množine $\mathcal{U}^0$. Dostávame nasledovné rezolventy:
    $$U^1 = \{ Q(f(h(b)),a),\, \neg P(h(b)),\, Q(f(c),a)\}$$. 
    \par
    $U^1$
    nie je prádzna a neobsahuje prádznu klauzulu -- musíme vytvoriť $U^2$.
    V tomto sa už vyskytne prádzna klauzula, čo znamená, že $C$ pohlcuje klauzulu
    $D$.
\end{priklad}

\begin{priklad}
    $C=P(x,x)$ a $D=P(f(x),y) \lor P(y,f(x))$. Zistite, či $C$
    je podklauzula $D$.

    \paragraph{Riešenie} (1) $x$, $y$ sú premenné v $D$. $a$ a $b$ sú konštanty,
    ktoré sa nevyskytujú $C$, $D$. $\Theta = \{ a/x, b/y\}$. $D\Theta = P(f(a),b), \lor P(b,
    f(a))$.

    $$\neg D\Theta = \neg P(f(a),b) \lor \neg O(b,f(a))$$
    $$W = \{ \neg P(f(a),b), \neg P(b,f(a))\}$$
    $$\mathcal{U}^0 = P(x,x)$$


    \par (2) $\mathcal{U}^0$ neobsahuje $\square$, tak sa môže zistiť
    $\mathcal{U}^1$
    \par (3) $\mathcal{U}^1 = \emptyset$. Záver: $C$ nie je podklauzula $D$.
\end{priklad}

\begin{priklad}
    Majme formuly:

    \begin{enumerate}
        \item $P\implies S$
        \item $S \implies U$
        \item $P$
        \item $U$
    \end{enumerate}

    Dokážte, že formula 4 vyplýva z formúl 1, 2 a 3. 

    \paragraph{Riešenie} Prepíšeme si formuly do správneho tvaru, aby sme mohli
    použiť pravidlo rezolventy:
    \begin{enumerate}
            \item $\neg P \lor S$
            \item $\neg S\lor U$
            \item $P$
            \item $U$
    \end{enumerate}
    Snažíme sa nájsť negáciu -- chceme ukázať, že 
    \begin{enumerate}
            \item $\neg P \lor S$
            \item $\neg S\lor U$
            \item $P$
            \item $\neg U$
    \end{enumerate}

    nie je splniteľná. Zoberiem si rezolventu 1 a 3, dostávam $S$ (5). Keď zoberiem 
    2 a 4, dostávam $\neg S$ (6). Zoberiem 5 a 6, dostávam $\square$ (7).
\end{priklad}


\begin{priklad}
    Predpoklad: Študenti sú občania. Záver: Hlasy študentov sú
    hlasy občanov.

    \paragraph{Riešenie} 
    \begin{itemize}
            \item $S(x)$ označuje \uv{$x$ je študent}.
            \item $C(x)$ označuje \uv{$x$ je občan}.
            \item $V(x,y)$ označuje \uv{$x$ je hlas $y$}.
    \end{itemize}
    Predpoklad: $(\forall y) (S(y)\implies C(y))$. Študenti sú občania.
    Záver: $(\forall x) ((\exists y) (S(y) \land V(x,y)) \implies (\exists z)(C(z)
    \implies V(x,z)))$. Hlasy študentov sú hlasy občanov.

    Aká bude štandardná forma pre vyjadrenie predpokladu?
    \begin{enumerate}
            \item $\neg S(y) \lor C(y)$
                \par $\neg ((\forall x) ((\exists y)(S(y)\land V(x,y)) \implies
                (\exists x)(C(z) \land V(x,z)))) \iff 
                \neg ((\forall x)(\forall y)(\neg S(y)\lor \neg V(x,y)) \lor
                (\exists z)(C(z)\land V(x,z))) \iff 
                \neg ((\forall x)(\forall y)(\exists x)(\neg S(y) \lor
                \neg U(x,y)\lor (C(z) \land V(x,z)))) \iff
                (\exists x)(\exists y)(\forall z) (S(y) \land V(x,y)) \land
                (\neg C(z) \lor \neg V(x,z))$
                Teraz potrebujeme Skolemov normálny tvar:
                $(\forall z)(S(b) \land U(a,b)) \land(\neg C(z) \lor \neg
                V(a,z)))$
                \par Pre negáciu záver dostávane nasledujúce klauzuly:
            \item $S(b)$
            \item $V(a,b)$
            \item $\neg C(z) \lor \neg V(a,z)$.

            \item $C(b)$ z (1) a (2) (miesto $y$ dosadíme $b$)
            \item $\neg V(a,b)$ zo (4) a (5)
            \item $\square$ z (3)  a (6)
    \end{enumerate}

    \par Predpokladajme, že $b$ je študent, $a$ je hlas študenta $b$ a nie je hlas
    žiadneho občana. Pretože $b$ je študent, $b$ je občan. Okrem toho $a$ nemôže byž
    hlas $b$, pretože $b$ je občan a to nie je možné.
\end{priklad}
